$\forall$$i$, $a$, $x$:Id, $X$, $T$:Type, $x_{0}$:$X$, $P$:($X$$\rightarrow$$T$$\rightarrow$Prop), ${\it es}$:ES. pre{-}init1{-}p(${\it es}$;$i$;$x$;$X$;$x_{0}$;$a$;$T$;$P$) $\in$ Prop